M:MsgA, dec:(a:Ids:M.stateDec(a in dom(M.pre) & (v:M.da(locl(a)). M.pre(a,s,v)))).
Chooser(dec)  b:IdM.state(M.da(locl(b))+Unit) 

latex

Definitions	t  T, x:A. B(x), M.pre(a,s,v), locl(a), M.da(a), x:AB(x), x:A. B(x), a in dom(M.pre), Type, A & B, inr(x), Prop, A, inl(x), left+right, P  Q, Dec(P), Void, x:AB(x), P  Q, False, f(a), MsgA, M.state, Id, , Unit, x.A(x), x. t(x), 2of(t), 1of(t), Case b of inl(x)  s(x) ; inr(y)  t(y), Chooser(dec)
Lemmas	pi1 wf, pi2 wf, unit wf, it wf, Id wf, ma-st wf, msga wf, decidable wf, not wf, ma-has-pre wf, ma-da wf, locl wf, ma-pre wf